package joc.nextgen;

import static joc.nextgen.JOC.post;
import static joc.nextgen.JOC.result;

import java.lang.ref.WeakReference;

class ObjectSpecContract implements ObjectSpec {
	private int hashCode;
	private boolean hashCodeSet = false;
	private WeakReference<Object> firstObject = null;

	@Override
	public boolean equals(Object obj) {
		if (firstObject == null || firstObject.get() == null) {
			firstObject = new WeakReference<Object>(obj);
		}
		if (post()) {
			if (obj == null) {
				assert result(boolean.class) == false : "if obj == null then false";
			} else {
				Object x = this;
				Object y = obj;
				Object z = firstObject.get();
				assert x.equals(x) : "is reflexive";
				assert x.equals(y) == y.equals(x) : "is symmetric";
				if (x.equals(y) && y.equals(z)) {
					assert x.equals(z) : "is transitive";
				}
				if (result(boolean.class)) {
					assert x.hashCode() == y.hashCode() : "is consistent with hashCode";
				}
			}
		}
		return false;
	}

	@Override
	public int hashCode() {
		if (!hashCodeSet) {
			hashCode = hashCode();
			hashCodeSet = true;
		}
		if (post()) {
			assert result(int.class) == hashCode : "is immutable";
		}
		return 0;
	}

	@Override
	public String toString() {
		if (post()) {
			assert result() != null : "not null";
		}
		return null;
	}

}